Formal verification of Hybrid Casper FFG

#Formal_verification #Casper

Background

Hybrid Casper FFG Original paper: Casper the Friendly Finality Gadget

Vitalik Buterin and Virgil Griffith

Protocol verification

Karl Palmskog

Runtime Verificationによるバイトコードの検証と並行して行われた

概要と結果 protocol-verification.md

GitHub Repo

paper Verification of Casper in the Coq proof assistant

Tech

Toychainをベースにしている

「フォーク」を扱っていたことがニーズに合っていた

具体的には以下を拝借

datatypes for blocks of transactions, blockchains, and block forest, and accompanying functions and lemmas (e.g., block validation)

datatypes and functions for (abstract) network node state

message processing functions and node/network behavior semantics

pirapiraさんのIsabelle/HOLによる検証プロジェクトを拡張している

GitHub Repo

Model

a static validator set

Toychain

Propaties

あくまでPoSによる投票・finalityのプロトコルのみ

Basically following white paper

Accountable safety

if two blocks are finalized and neither is an ancestor of the other, then validators having at least 1/3 of the deposits must have violated the slashing conditions.

nrryuya.icon > "For any pair of finalized blocks either is an ancestor of the other" is only one property to be satisfied.

Plausible liveness

as long as at least 2/3 of validators are following the protocol and block proposals continue, then further checkpoints can continue to be finalized regardless of the behavior of the less the 1/3 of misbehaving validators, without needing any of the honest validators to violate a slashing condition and sacrifice their deposit to allow the chain to live.

Protocol to bytecode

3 specs in K

abstract casper: プロトコルの形式的検証チームとの橋渡し

casper: high-levelだが、reward/penaltyの計算をepochごとではなくvoteごとに行うなど厳密にした

casper evm: EVMレベルのspec(gas consumption, storage layout, arithmetic overflowなどを含む)

encoding ABSTRACT-CASPER in Coq

Bytecode verification

発見したバグ

バリデーターのvote時のepochのチェック箇所の誤り

target_hashのチェックの直後にチェックするように

code: casper(python)

assert target_hash == self.get_recommended_target_hash()